(declare-sort S 0)

(declare-fun TS0 () S)
(declare-fun S0 () S)
(declare-fun |N(0, 0)| () Bool)
(declare-fun TS1 () S)
(declare-fun S1 () S)
(declare-fun |N(1, 0)| () Bool)
(declare-fun S2 () S)
(declare-fun S14 () S)
(declare-fun TS6 () S)
(declare-fun S6 () S)
(declare-fun |N(6, 0)| () Bool)
(declare-fun TS7 () S)
(declare-fun S7 () S)
(declare-fun |N(7, 0)| () Bool)
(declare-fun TS12 () S)
(declare-fun S12 () S)
(declare-fun |N(12, 0)| () Bool)
(declare-fun TS13 () S)
(declare-fun S13 () S)
(declare-fun |N(13, 0)| () Bool)
(declare-fun TS14 () S)
(declare-fun |N(14, 1)| () Bool)
(declare-fun TS19 () S)
(declare-fun S19 () S)
(declare-fun |N(19, 0)| () Bool)
(assert (=> |N(0, 0)| (and and (and (distinct S0 TS0) true) ((_ tree-order 0) S0 TS0))))
(assert (=> |N(1, 0)| (and and (and (distinct S1 TS1) true) ((_ tree-order 0) S1 TS1))))
(assert (let (($x125 ((_ tree-order 0) S6 TS6))) (=> |N(6, 0)| (and (and (= S1 TS6)) (and (distinct S6 TS6) true) $x125))))
(assert (let (($x131 ((_ tree-order 0) S7 TS7))) (let (($x130 (and (distinct S7 TS7) true))) (=> |N(7, 0)| (and (and (= S2 TS7)) $x130 $x131)))))
(assert (let (($x142 ((_ tree-order 0) S12 TS12))) (=> |N(12, 0)| (and (and (= S1 TS12)) (and (distinct S12 TS12) true) $x142))))
(assert (let (($x148 ((_ tree-order 0) S13 TS13))) (=> |N(13, 0)| (and (and (= S1 TS13)) (and (distinct S13 TS13) true) $x148))))
(assert (let (($x155 ((_ tree-order 0) S14 TS14))) (let (($x154 (and (distinct S14 TS14) true))) (=> |N(14, 1)| (and (and (= S2 TS14)) $x154 $x155)))))
(assert (let (($x166 ((_ tree-order 0) S19 TS19))) (let (($x167 (and (and (= S13 TS19) (= S6 TS19)) (and (distinct S19 TS19) true) $x166))) (=> |N(19, 0)| $x167))))
(check-sat)
